$\forall$$k$:Knd, $l$:IdLnk, ${\it dt}$:fpf(Id; $x$.Type).
\\[0ex]($\uparrow$fpf{-}dom(Kind{-}deq; $k$; lnk{-}decl($l$; ${\it dt}$)))
\\[0ex]$\Rightarrow$ guard((($\uparrow$isrcv($k$)) c$\wedge$ ($\uparrow$fpf{-}dom(id{-}deq; tag($k$); ${\it dt}$))))